\begin{tabbing}
$\forall$$M_{1}$, $M_{2}$:MsgA.
\\[0ex]$M_{1}$ $\subseteq$ $M_{2}$
\\[0ex]$\Rightarrow$ \=(\=$\forall$$k$:Knd, $l$:IdLnk, $s$:$M_{2}$.state, $v$:$M_{2}$.da($k$), $i$:Id,\+\+
\\[0ex]${\it ms}$:((${\it tg}$:Id $\times$ if source($l$) = $i$ then $M_{2}$.da(rcv($l$,${\it tg}$)) else Top fi ) List).
\-\\[0ex]$M_{2}$.send($k$;$l$;$s$;$v$;${\it ms}$;$i$) $\Rightarrow$ $M_{1}$.send($k$;$l$;$s$;$v$;${\it ms}$;$i$))
\-
\end{tabbing}